(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (or (not (>= (+ (* (- 2) c) a b) (- 5))) (< (+ (* (- 46) b) (* (- 22) c)) 0)))
(push)
(assert (or (not (< (+ c a) 2)) (> a 7)))
(check-sat)
(pop)
(assert (or (> (+ b a) 2) (= (+ (* 30 b) a (* 8 11 c)) 0)))
(assert (<= b 0))
(push)
(assert (> (+ (* (- 3) c) (* (- 7) a)) 3))
(check-sat)
(pop)
(assert (<= (+ (* (- 33) a) (* (- 7) c)) 4))
(assert (> (+ (* 30 a) (* 17 a) (* (- 48) a)) 9))
(check-sat)
(check-sat)
(assert (not (= (* 4 c) 8)))
(assert (or (> 0 c) (not (< (* 38 c) 5))))
(assert (or (>= (- 33) 2) (not (>= (* 17 c) 41)) (>= (mod (to_int (* 28 b)) (to_int (* (- 2) a))) 0)))
(assert (or (= (+ (mod 4 (to_int a)) (* (- 22) b)) 0) (<= b 7)))
(check-sat)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (or (not (>= (+ (* (- 2) c) a b) (- 5))) (< (+ (* (- 46) b) (* (- 22) c)) 0)))
(push)
(assert (or (not (< (+ c a) 2)) (> a 7)))
(check-sat)
(pop)
(assert (or (> (+ b a) 2) (= (+ (* 30 b) a (* 8 11 c)) 0)))
(assert (<= b 0))
(push)
(assert (> (+ (* (- 3) c) (* (- 7) a)) 3))
(check-sat)
(pop)
(assert (<= (+ (* (- 33) a) (* (- 7) c)) 4))
(assert (> (+ (* 30 a) (* 17 a) (* (- 48) a)) 9))
(check-sat)
(check-sat)
(assert (not (= (* 4 c) 8)))
(assert (or (> 0 c) (not (< (* 38 c) 5))))
(assert (or (>= (- 33) 2) (not (>= (* 17 c) 41)) (>= (mod (to_int (* 28 b)) (to_int (* (- 2) a))) 0)))
(assert (or (= (+ (mod 4 (to_int a)) (* (- 22) b)) 0) (<= b 7)))
(check-sat)
